(DEFPROP PRFFNS
 (PRFFNS PRFMAX PRFMIN RECTIFY COMMONTAIL COMMONHEAD)
VALUE)

(DEFPROP PRFMAX
 (LAMBDA(U PRMAX PRMIN ALPHA BETA)
  (COND	((NULL U) (LIST ALPHA PRMAX PRMIN))
	(T
	 ((LAMBDA(S)
	   (COND ((NOT (GREATERP (CAR S) ALPHA)) (PRFMAX (CDR U) PRMAX (CONS (CADDR S) PRMIN) ALPHA BETA))
		 ((LESSP (CAR S) BETA)
		  (PRFMAX (CDR U) (CONS (CAR U) (CADR S)) (CONS (CADDR S) PRMIN) (CAR S) BETA))
		 (T (LIST BETA (CONS (CAR U) (CADR S)) NIL))))
	  (COND	((TER (RECTIFY (CAR U)) ALPHA BETA) (LIST (IMVAL (RECTIFY (CAR U)))))
		(T (PRFMIN (SUCCESSORS (RECTIFY (CAR U))) NIL NIL ALPHA BETA)))))))
EXPR)

(DEFPROP PRFMIN
 (LAMBDA(U PRMAX PRMIN ALPHA BETA)
  (COND	((NULL U) (LIST BETA PRMAX PRMIN))
	(T
	 ((LAMBDA(S)
	   (COND ((NOT (GREATERP (CAR S) ALPHA)) (LIST ALPHA NIL (CONS (CAR U) (CADDR S))))
		 ((LESSP (CAR S) BETA)
		  (PRFMIN (CDR U) (CONS (CADR U) PRMAX) (CONS (CAR U) (CADDR S)) ALPHA (CAR S)))
		 (T (PRFMIN (CDR U) (CONS (CADR S) PRMAX) PRMIN ALPHA BETA))))
	  (COND	((TER (RECTIFY (CAR U)) ALPHA BETA) (LIST (IMVAL (RECTIFY (CAR U)))))
		(T (PRFMAX (SUCCESSORS (RECTIFY (CAR U))) NIL NIL ALPHA BETA)))))))
EXPR)

(DEFPROP RECTIFY
 (LAMBDA(P)
  (PROG	(Z Q)
	(SETQ Q (COMMONTAIL P P1))
   L1	(COND ((EQUAL Q P1) (GO L2)))
	(REVERT)
	(GO L1)
   L2	(SETQ Z (LISTSUBT P P1))
   L3	(COND ((NULL Z) (RETURN P)))
	(UPDATE (CAR Z))
	(SETQ Z (CDR Z))
	(GO L3)))
EXPR)

(DEFPROP COMMONTAIL
 (LAMBDA (U V) (REVERSE (COMMONHEAD (REVERSE U) (REVERSE V))))
EXPR)

(DEFPROP COMMONHEAD
 (LAMBDA(U V)
  (COND	((OR (NULL U) (NULL V) (NOT (EQUAL (CAR U) (CAR V)))) NIL)
	(T (CONS (CAR U) (COMMONHEAD (CDR U) (CDR V))))))
EXPR)